'Weak Dependency Graph [60.0]' ------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { zeros() -> cons(0(), n__zeros()) , tail(cons(X, XS)) -> activate(XS) , zeros() -> n__zeros() , activate(n__zeros()) -> zeros() , activate(X) -> X} Details: We have computed the following set of weak (innermost) dependency pairs: { zeros^#() -> c_0() , tail^#(cons(X, XS)) -> c_1(activate^#(XS)) , zeros^#() -> c_2() , activate^#(n__zeros()) -> c_3(zeros^#()) , activate^#(X) -> c_4()} The usable rules are: {} The estimated dependency graph contains the following edges: {tail^#(cons(X, XS)) -> c_1(activate^#(XS))} ==> {activate^#(n__zeros()) -> c_3(zeros^#())} {tail^#(cons(X, XS)) -> c_1(activate^#(XS))} ==> {activate^#(X) -> c_4()} {activate^#(n__zeros()) -> c_3(zeros^#())} ==> {zeros^#() -> c_2()} {activate^#(n__zeros()) -> c_3(zeros^#())} ==> {zeros^#() -> c_0()} We consider the following path(s): 1) { tail^#(cons(X, XS)) -> c_1(activate^#(XS)) , activate^#(n__zeros()) -> c_3(zeros^#()) , zeros^#() -> c_2()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: zeros() = [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] 0() = [0] n__zeros() = [0] tail(x1) = [0] x1 + [0] activate(x1) = [0] x1 + [0] zeros^#() = [0] c_0() = [0] tail^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] activate^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {zeros^#() -> c_2()} Weak Rules: { activate^#(n__zeros()) -> c_3(zeros^#()) , tail^#(cons(X, XS)) -> c_1(activate^#(XS))} Details: We apply the weight gap principle, strictly orienting the rules {zeros^#() -> c_2()} and weakly orienting the rules { activate^#(n__zeros()) -> c_3(zeros^#()) , tail^#(cons(X, XS)) -> c_1(activate^#(XS))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {zeros^#() -> c_2()} Details: Interpretation Functions: zeros() = [0] cons(x1, x2) = [1] x1 + [1] x2 + [8] 0() = [0] n__zeros() = [0] tail(x1) = [0] x1 + [0] activate(x1) = [0] x1 + [0] zeros^#() = [1] c_0() = [0] tail^#(x1) = [1] x1 + [9] c_1(x1) = [1] x1 + [0] activate^#(x1) = [1] x1 + [1] c_2() = [0] c_3(x1) = [1] x1 + [0] c_4() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { zeros^#() -> c_2() , activate^#(n__zeros()) -> c_3(zeros^#()) , tail^#(cons(X, XS)) -> c_1(activate^#(XS))} Details: The given problem does not contain any strict rules 2) { tail^#(cons(X, XS)) -> c_1(activate^#(XS)) , activate^#(n__zeros()) -> c_3(zeros^#()) , zeros^#() -> c_0()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: zeros() = [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] 0() = [0] n__zeros() = [0] tail(x1) = [0] x1 + [0] activate(x1) = [0] x1 + [0] zeros^#() = [0] c_0() = [0] tail^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] activate^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {zeros^#() -> c_0()} Weak Rules: { activate^#(n__zeros()) -> c_3(zeros^#()) , tail^#(cons(X, XS)) -> c_1(activate^#(XS))} Details: We apply the weight gap principle, strictly orienting the rules {zeros^#() -> c_0()} and weakly orienting the rules { activate^#(n__zeros()) -> c_3(zeros^#()) , tail^#(cons(X, XS)) -> c_1(activate^#(XS))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {zeros^#() -> c_0()} Details: Interpretation Functions: zeros() = [0] cons(x1, x2) = [1] x1 + [1] x2 + [8] 0() = [0] n__zeros() = [0] tail(x1) = [0] x1 + [0] activate(x1) = [0] x1 + [0] zeros^#() = [1] c_0() = [0] tail^#(x1) = [1] x1 + [9] c_1(x1) = [1] x1 + [0] activate^#(x1) = [1] x1 + [1] c_2() = [0] c_3(x1) = [1] x1 + [0] c_4() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { zeros^#() -> c_0() , activate^#(n__zeros()) -> c_3(zeros^#()) , tail^#(cons(X, XS)) -> c_1(activate^#(XS))} Details: The given problem does not contain any strict rules 3) { tail^#(cons(X, XS)) -> c_1(activate^#(XS)) , activate^#(n__zeros()) -> c_3(zeros^#())} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: zeros() = [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] 0() = [0] n__zeros() = [0] tail(x1) = [0] x1 + [0] activate(x1) = [0] x1 + [0] zeros^#() = [0] c_0() = [0] tail^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] activate^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {activate^#(n__zeros()) -> c_3(zeros^#())} Weak Rules: {tail^#(cons(X, XS)) -> c_1(activate^#(XS))} Details: We apply the weight gap principle, strictly orienting the rules {activate^#(n__zeros()) -> c_3(zeros^#())} and weakly orienting the rules {tail^#(cons(X, XS)) -> c_1(activate^#(XS))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {activate^#(n__zeros()) -> c_3(zeros^#())} Details: Interpretation Functions: zeros() = [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] 0() = [0] n__zeros() = [0] tail(x1) = [0] x1 + [0] activate(x1) = [0] x1 + [0] zeros^#() = [0] c_0() = [0] tail^#(x1) = [1] x1 + [1] c_1(x1) = [1] x1 + [0] activate^#(x1) = [1] x1 + [1] c_2() = [0] c_3(x1) = [1] x1 + [0] c_4() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { activate^#(n__zeros()) -> c_3(zeros^#()) , tail^#(cons(X, XS)) -> c_1(activate^#(XS))} Details: The given problem does not contain any strict rules 4) {tail^#(cons(X, XS)) -> c_1(activate^#(XS))} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: zeros() = [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] 0() = [0] n__zeros() = [0] tail(x1) = [0] x1 + [0] activate(x1) = [0] x1 + [0] zeros^#() = [0] c_0() = [0] tail^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] activate^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {tail^#(cons(X, XS)) -> c_1(activate^#(XS))} Weak Rules: {} Details: We apply the weight gap principle, strictly orienting the rules {tail^#(cons(X, XS)) -> c_1(activate^#(XS))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {tail^#(cons(X, XS)) -> c_1(activate^#(XS))} Details: Interpretation Functions: zeros() = [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] 0() = [0] n__zeros() = [0] tail(x1) = [0] x1 + [0] activate(x1) = [0] x1 + [0] zeros^#() = [0] c_0() = [0] tail^#(x1) = [1] x1 + [1] c_1(x1) = [1] x1 + [0] activate^#(x1) = [1] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: {tail^#(cons(X, XS)) -> c_1(activate^#(XS))} Details: The given problem does not contain any strict rules 5) { tail^#(cons(X, XS)) -> c_1(activate^#(XS)) , activate^#(X) -> c_4()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: zeros() = [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] 0() = [0] n__zeros() = [0] tail(x1) = [0] x1 + [0] activate(x1) = [0] x1 + [0] zeros^#() = [0] c_0() = [0] tail^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] activate^#(x1) = [0] x1 + [0] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {activate^#(X) -> c_4()} Weak Rules: {tail^#(cons(X, XS)) -> c_1(activate^#(XS))} Details: We apply the weight gap principle, strictly orienting the rules {activate^#(X) -> c_4()} and weakly orienting the rules {tail^#(cons(X, XS)) -> c_1(activate^#(XS))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {activate^#(X) -> c_4()} Details: Interpretation Functions: zeros() = [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] 0() = [0] n__zeros() = [0] tail(x1) = [0] x1 + [0] activate(x1) = [0] x1 + [0] zeros^#() = [0] c_0() = [0] tail^#(x1) = [1] x1 + [1] c_1(x1) = [1] x1 + [0] activate^#(x1) = [1] x1 + [1] c_2() = [0] c_3(x1) = [0] x1 + [0] c_4() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { activate^#(X) -> c_4() , tail^#(cons(X, XS)) -> c_1(activate^#(XS))} Details: The given problem does not contain any strict rules